<
logic> A set of
atomic literals with at most one {positive
literal}. Usually written
L < - L1, ..., Ln
or
< - L1, ..., Ln
where n >= 0, " < - " means "is implied by" and comma stands for
conjuction ("AND"). If L is false the
clause is regarded as
a
goal.
Horn clauses can express a subset of statements of
first order logic.
The name "
Horn Clause" comes from the logician Alfred
Horn,
who first pointed out the significance of such
clauses in
1951, in the article "On sentences which are true of direct
unions of algebras", Journal of Symbolic Logic, 16, 14-21.
A
definite clause is a
Horn clause that has exactly one
positive literal.
(2000-01-24)